A, B:Type, f:(AB), L:(A List), L1, L2:(B List).
(map(f;L) = (L1 @ L2)  (B List))
 {map(f;firstn(||L1||;L)) = L1 & map(f;nth_tl(||L1||;L)) = L2} 

latex

Definitions	x:A. B(x), map(f;as), {T}, firstn(n;as), Y, t  T, P  Q, P & Q, nth_tl(n;as), ||as||, if b then t else f fi , i z j, tl(l), b, i <z j, tt, ff, , Top, S  T, i  j , P  Q, P  Q, T, True, as @ bs, hd(l), , Unit,
Lemmas	append is nil, map wf, ifthenelse wf, le int wf, length wf1, nth tl wf, append wf, first0, top wf, non neg length, map length, ge wf, hd wf, tl wf, lt int wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of lt int, le wf, assert of le int, bnot wf, eqff to assert, bnot of le int, squash wf, true wf, bnot of lt int